Nuprl Lemma : decidable__es-causle
11,40
postcript
pdf
the_es
:ES,
e'
,
e
:E. Dec(
e
c
e'
)
latex
Definitions
t
T
,
,
e
c
e'
,
x
:
A
.
B
(
x
)
,
P
Q
Lemmas
event
system
wf
,
es-E
wf
,
decidable
es-E-equal
,
decidable
es-causl
,
es-causl
wf
,
decidable
or
origin
the_es:ES, e', e:E. Dec(e c
e') the_es:ES, e', e:E. Dec(e c e') 
T
e'x:A. B(x)
Q